In \hyperref[sec:prototype]{this section}, we comment on  some aspects of our implementation and show a system session
 for our running example. The SQL Test Case Generator
(\textit{STCG}) is implemented in the programming language C++.


The input of STCG consists of a table or view name $R$, and a SQL file containing the definition of $R$ and
of all the relations in its syntactic dependence tree.
The goal is to obtain a positive test-case for $R$.

STCG can be seen as a pipeline, which helps to maintain and extend the implementation.
In a first phase the prototype generates a representation in C++ of the CSP. This phase
consists of two steps:

\begin{enumerate}
  \item \textbf{SQL parser}: STCG includes a SQL parser to
     pre-process the input file. The result is a C++
    representation of the database schema. This parser has been produced using
    \textit{GNU Bison} \cite{Bison}, a general-purpose parser generator, and
    \textit{Flex} \cite{Flex}, a tool for generating scanners.

  \item \textbf{Formula Generator}: The core of STCG. Takes as input
    the output of the previous step, and following Definition \ref{def:constraints}
    described in Section \ref{sec:constraints}, generates the first order logic formula
    representing the constraints associated to  the table or view specified.
\end{enumerate}

\begin{figure}
  \centering
    \includegraphics[width=1.00\textwidth]{pipeline1}
    \caption{Pipeline of STCG.}
    \label{fig:pipeline1}
\end{figure}


Figure \ref{fig:pipeline1} shows a diagram of this first phase.
Next, we want to satisfy this formula by binding the logic
variables, thus obtaining a positive test case if possible.

\begin{figure}
  \centering
    \includegraphics[width=1.00\textwidth]{pipeline2}
    \caption{Pipeline of STCG extended with an input builder for a solver.}
    \label{fig:pipeline2}
\end{figure}

In the second phase (see Figure \ref{fig:pipeline2}) the logic formula is translated into a
format accepted by some external constraint solver.
We have used \textit{G12/CPX} as solver, which is
distributed with \textit{G12 MiniZinc distribution}, however, any solver that implements FlatZinc can be used for this purpose. \textit{MiniZinc} \cite{MiniZinc}
is a medium-level constraint modeling language. We translate our
logic formula into a \textit{MiniZinc model}, so it can be solved,
returning, if possible, the positive test-cases. Other
constraint programing languages can be added by implementing new translators.

Below we present a system session for the example at
hand. Consider that the input SQL file corresponds to Example \ref{ex:running}.

Following the pipeline, the SQL parser  takes this file as input and
generates an internal  C++ representation of the database schema (it
can be obtained at the command line using the "-v" option of STCG).
Suppose that the user intends to
generate a test case for view \textit{checked}  indicating that tables
\textit{player} and \textit{board} must have two rows at most.
 Thus, the \textit{Formula Generator} module takes the
database schema as input and generates the following formula (where
symbolic variables are of the form \textit{table name.column name.row}):

{\small \noindent
\begin{verbatim}
#(checked)=
 {(((((board.id.0 ==  player.id.0) OR (board.id.1 == player.id.0))
 AND ... 
 (not (((((board.x.0 - board.x.1) * (board.y.0 - board.y.1)) == 0)
 AND (board.id.1 != board.id.0)) OR ...))))),
 {checked.id -> player.id.0}), ...}
\end{verbatim}
}

This corresponds to $\theta(checked,board)$ without considering primary and foreign keys (displayed below).
For the sake of space we display only part of the first formula and the first row \cod{\{checked.id $\rightarrow$ player.id.0\}}.
This row indicates that all the pieces of \cod{player.id.0} are checked if the formula holds.
Firstly, the formula indicates that \cod{player.id.0} must have a piece on either the position corresponding to
\cod{board.id.0} or to \cod{board.id.1}. The other part of the formula displayed indicates that there is a check
between positions contained in \cod{board.x.0,board.y.0}, and \cod{board.x.1,board.y.1} for two different players.

Primary key constraint of table \textit{player} is shown below. For
simplicity, only logic formula for the first row \cod{\{player.id
  $\rightarrow$ player.id.0\}} is displayed. That formula indicates that
this table cannot have two players with the same \cod{id} attribute,
that is \cod{player.id.0 != player.id.1}.

{\small
\begin{verbatim}
  #(player)={(player.id.0 != player.id.1),
  {player.id -> player.id.0}), ...}
\end{verbatim}
}

Next, we display primary key and foreign key constraints of
\textit{board} for the first row \cod{\{board.x $\rightarrow$ board.x.0,
  board.y $\rightarrow$ board.y.0, board.id $\rightarrow$
  board.id.0\}}. That formula indicates that \cod{id} attribute of
each row of this table must reference one of \cod{id} attributes of the
table \textit{player} (foreign key), that is \cod{board.id.0 == player.id.0 $\land$
  board.id.1 == player.id.0}, and two pieces cannot be in the same
game board position, that is \cod{(board.x.0 != board.x.1) $\lor$
  (board.y.0 != board.y.1)} (primary key).

{\small
\begin{verbatim}
#(board)=
{(((board.id.0 == player.id.0) AND (board.id.1 == player.id.0))
AND ((board.x.0 != board.x.1) OR (board.y.0 != board.y.1)),
{board.x-> board.x.0,board.y-> board.y.0,board.id-> board.id.0}),...}
\end{verbatim}
}

Actually, STCG generates only one formula, with primary key and
foreign key constraints included, but we show them separated for
simplicity.

The next step of the pipeline is to solve this constraints if
possible. As mentioned above, we use the MiniZinc constraint modeling
language for this purpose. We introduce a new step to the pipeline, that will translate our
\textit{Formula} to a \textit{MiniZinc model}. This model consists of four 
sections: variable declarations, constraint specification, solver invocation and output formatting.

The model is saved in a file that can be later executed by MiniZinc,
returning the positive test-case if possible. To obtain meaningful
results we restrict the domain of symbolic variables to 1..5 in this
session. In the future, our tool will support domain constraints of
symbolic variables. The result returned by MiniZinc is:

\begin{verbatim}
INSERT INTO board(id,x,y) VALUES (1,1,1);
INSERT INTO board(id,x,y) VALUES (2,1,5);
INSERT INTO player(id) VALUES(1);
INSERT INTO player(id) VALUES(2);
\end{verbatim}

This result is a positive test-case, written as a set of SQL insert statements that populates the tables of the database as shown in Table \ref{testcase}.

\begin{table}[ht]
\centering
\subfloat[Positive test-case for table player][Player]{
\begin{tabular}{|c|}
\hline
{\textbf{player}} \\
\hline
id \\
\hline
$1$ \\
$2$ \\
\hline
\end{tabular}}
\qquad
\subfloat[Positive test-case for table board][Board]{\begin{tabular}{|c|c|c|}
\hline
\multicolumn{3}{|c|}{\textbf{board}} \\
\hline
id & x & y \\
\hline
$1$ & $1$ &  $1$ \\
$2$ & $1$ &  $5$ \\
\hline
\end{tabular}}
\caption{Positive test-case}\label{testcase}
\end{table}


Thus, the board has player 1 in position (1,1) and player 2 in position (1,5) and both players are \cod{checked} as defined in the example \ref{ex:running}. We can check that this instance is a positive test-case by executing the SQL query \cod{select * from checked}, which returns the non empty result shown in Table \ref{result}.

\begin{table}
\centering
\begin{tabular}{|c|}
\hline
id \\
\hline
$1$ \\
$2$ \\
\hline
\end{tabular}
\caption{Select * from checked}\label{result}
\end{table}



